Nuprl Lemma : rel_inverse_wf
4,23
postcript
pdf
T1
,
T2
:Type,
R
:(
T1
T2
Prop).
R
^-1
T2
T1
Prop
latex
Definitions
R
^-1
,
x
:
A
.
B
(
x
)
,
x
f
y
,
Prop
,
t
T
origin
T1, T2:Type, R:(T1
T2Prop). R^-1 
T2T1Prop T1, T2:Type, R:(T1T2Prop). R^-1 T2T1Prop x:A. B(x) T